This paper continues investigations in "synthetic homotopy theory": the useof homotopy type theory to give machine-checked proofs of constructions fromhomotopy theory We present a mechanized proof of the Blakers-Massey connectivity theorem, aresult relating the higher-dimensional homotopy groups of a pushout type(roughly, a space constructed by gluing two spaces along a shared subspace) tothose of the components of the pushout. This theorem gives importantinformation about the pushout type, and has a number of useful corollaries,including the Freudenthal suspension theorem, which has been studied inprevious formalizations. The new proof is more elementary than existing ones in abstracthomotopy-theoretic settings, and the mechanization is concise and high-level,thanks to novel combinations of ideas from homotopy theory and type theory.
展开▼
